Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

circ(cons(a, s), t) → cons(msubst(a, t), circ(s, t))
circ(cons(lift, s), cons(a, t)) → cons(a, circ(s, t))
circ(cons(lift, s), cons(lift, t)) → cons(lift, circ(s, t))
circ(circ(s, t), u) → circ(s, circ(t, u))
circ(s, id) → s
circ(id, s) → s
circ(cons(lift, s), circ(cons(lift, t), u)) → circ(cons(lift, circ(s, t)), u)
subst(a, id) → a
msubst(a, id) → a
msubst(msubst(a, s), t) → msubst(a, circ(s, t))

Q is empty.


↳ QTRS
  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

circ(cons(a, s), t) → cons(msubst(a, t), circ(s, t))
circ(cons(lift, s), cons(a, t)) → cons(a, circ(s, t))
circ(cons(lift, s), cons(lift, t)) → cons(lift, circ(s, t))
circ(circ(s, t), u) → circ(s, circ(t, u))
circ(s, id) → s
circ(id, s) → s
circ(cons(lift, s), circ(cons(lift, t), u)) → circ(cons(lift, circ(s, t)), u)
subst(a, id) → a
msubst(a, id) → a
msubst(msubst(a, s), t) → msubst(a, circ(s, t))

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

CIRC(circ(s, t), u) → CIRC(s, circ(t, u))
CIRC(cons(a, s), t) → MSUBST(a, t)
MSUBST(msubst(a, s), t) → MSUBST(a, circ(s, t))
CIRC(circ(s, t), u) → CIRC(t, u)
CIRC(cons(lift, s), cons(a, t)) → CIRC(s, t)
CIRC(cons(lift, s), circ(cons(lift, t), u)) → CIRC(s, t)
CIRC(cons(a, s), t) → CIRC(s, t)
CIRC(cons(lift, s), circ(cons(lift, t), u)) → CIRC(cons(lift, circ(s, t)), u)
MSUBST(msubst(a, s), t) → CIRC(s, t)
CIRC(cons(lift, s), cons(lift, t)) → CIRC(s, t)

The TRS R consists of the following rules:

circ(cons(a, s), t) → cons(msubst(a, t), circ(s, t))
circ(cons(lift, s), cons(a, t)) → cons(a, circ(s, t))
circ(cons(lift, s), cons(lift, t)) → cons(lift, circ(s, t))
circ(circ(s, t), u) → circ(s, circ(t, u))
circ(s, id) → s
circ(id, s) → s
circ(cons(lift, s), circ(cons(lift, t), u)) → circ(cons(lift, circ(s, t)), u)
subst(a, id) → a
msubst(a, id) → a
msubst(msubst(a, s), t) → msubst(a, circ(s, t))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof

Q DP problem:
The TRS P consists of the following rules:

CIRC(circ(s, t), u) → CIRC(s, circ(t, u))
CIRC(cons(a, s), t) → MSUBST(a, t)
MSUBST(msubst(a, s), t) → MSUBST(a, circ(s, t))
CIRC(circ(s, t), u) → CIRC(t, u)
CIRC(cons(lift, s), cons(a, t)) → CIRC(s, t)
CIRC(cons(lift, s), circ(cons(lift, t), u)) → CIRC(s, t)
CIRC(cons(a, s), t) → CIRC(s, t)
CIRC(cons(lift, s), circ(cons(lift, t), u)) → CIRC(cons(lift, circ(s, t)), u)
MSUBST(msubst(a, s), t) → CIRC(s, t)
CIRC(cons(lift, s), cons(lift, t)) → CIRC(s, t)

The TRS R consists of the following rules:

circ(cons(a, s), t) → cons(msubst(a, t), circ(s, t))
circ(cons(lift, s), cons(a, t)) → cons(a, circ(s, t))
circ(cons(lift, s), cons(lift, t)) → cons(lift, circ(s, t))
circ(circ(s, t), u) → circ(s, circ(t, u))
circ(s, id) → s
circ(id, s) → s
circ(cons(lift, s), circ(cons(lift, t), u)) → circ(cons(lift, circ(s, t)), u)
subst(a, id) → a
msubst(a, id) → a
msubst(msubst(a, s), t) → msubst(a, circ(s, t))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We deleted some edges using various graph approximations

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ EdgeDeletionProof
        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CIRC(circ(s, t), u) → CIRC(s, circ(t, u))
CIRC(cons(a, s), t) → MSUBST(a, t)
MSUBST(msubst(a, s), t) → MSUBST(a, circ(s, t))
CIRC(circ(s, t), u) → CIRC(t, u)
CIRC(cons(lift, s), cons(a, t)) → CIRC(s, t)
CIRC(cons(a, s), t) → CIRC(s, t)
CIRC(cons(lift, s), circ(cons(lift, t), u)) → CIRC(s, t)
CIRC(cons(lift, s), circ(cons(lift, t), u)) → CIRC(cons(lift, circ(s, t)), u)
MSUBST(msubst(a, s), t) → CIRC(s, t)
CIRC(cons(lift, s), cons(lift, t)) → CIRC(s, t)

The TRS R consists of the following rules:

circ(cons(a, s), t) → cons(msubst(a, t), circ(s, t))
circ(cons(lift, s), cons(a, t)) → cons(a, circ(s, t))
circ(cons(lift, s), cons(lift, t)) → cons(lift, circ(s, t))
circ(circ(s, t), u) → circ(s, circ(t, u))
circ(s, id) → s
circ(id, s) → s
circ(cons(lift, s), circ(cons(lift, t), u)) → circ(cons(lift, circ(s, t)), u)
subst(a, id) → a
msubst(a, id) → a
msubst(msubst(a, s), t) → msubst(a, circ(s, t))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.